Nuprl Lemma : ma-random_wf
11,40
postcript
pdf
M
:MsgA,
T
:Type,
v
:
T
,
i
,
a
:Id,
n
:
. ma-random(
M
;
T
;
v
;
i
;
a
;
n
)
latex
Definitions
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
b
,
Type
,
Id
,
,
x
.
t
(
x
)
,
FinProbSpace
,
a
:
A
fp
B
(
a
)
,
Top
,
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
)}
,
Atom$n
,
x
dom(
f
)
,
random(
p
;
a
;
b
)
,
f
(
a
)
,
s
=
t
,
Outcome
,
,
A
c
B
,
IdDeq
,
x
.
A
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
z
!=
f
(
x
)
P
(
a
;
z
)
,
ma-random(
M
;
T
;
v
;
i
;
a
;
n
)
,
x
:
A
B
(
x
)
,
MsgA
Lemmas
msga
wf
,
fpf-val
wf
,
id-deq
wf
,
p-outcome
wf
,
random
wf
,
finite-prob-space
wf
,
assert
wf
,
fpf-dom
wf
,
fpf-trivial-subtype-top
,
nat
wf
,
Id
wf
origin
M:MsgA, T:Type, v:T, i, a:Id, n:
. ma-random(M;T;v;i;a;n) 
M:MsgA, T:Type, v:T, i, a:Id, n:. ma-random(M;T;v;i;a;n) T
B(x)x:A. B(x)
b
x. t(x) B(a)
Q
A
B
dom(f)
Bx.A(x)x,y. t(x;y) P(a;z)
B(x)